Nuprl Definition : hgrp_of_ocgrp
13,42
postcript
pdf
g
hgrp == <|
g
|
, =
,
, *, e,
x
.
x
>
latex
clarification:
g
hgrp == <|
g
|
, =
g
,
g
, *
g
, e
g
,
x
.
x
>
latex
Up
groups
1
Wellformedness Lemmas
hgrp
of
ocgrp
wf
,
hgrp
of
ocgrp
wf2
Definitions
|
g
|
,
=
,
,
*
,
e
origin
hgrp == <|g|
, =
, 
, *, e, 
x.x>
hgrp == <|g|, =g, g, *g, eg, x.x> hgrp == <|g|, =, , *, e, x.x>
hgrp == <|g|, =g, g, *g, eg, x.x>